Termination w.r.t. Q proof of TRS/Cimelse.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

TERM_SUB(Term_sub(m, s), t) → CONCAT(s, t)
TERM_SUB(Term_sub(m, s), t) → TERM_SUB(m, Concat(s, t))
TERM_SUB(Case(m, xi, n), s) → FROZEN(m, Sum_sub(xi, s), n, s)
TERM_SUB(Term_inl(m), s) → TERM_SUB(m, s)
TERM_SUB(Term_var(x), Cons_usual(y, m, s)) → TERM_SUB(Term_var(x), s)
CONCAT(Cons_usual(x, m, s), t) → CONCAT(s, t)
CONCAT(Concat(s, t), u) → CONCAT(s, Concat(t, u))
CONCAT(Cons_usual(x, m, s), t) → TERM_SUB(m, t)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(n, s)
TERM_SUB(Case(m, xi, n), s) → SUM_SUB(xi, s)
FROZEN(m, Sum_constant(Right), n, s) → TERM_SUB(n, s)
CONCAT(Concat(s, t), u) → CONCAT(t, u)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(n, s)
TERM_SUB(Term_inr(m), s) → TERM_SUB(m, s)
FROZEN(m, Sum_constant(Left), n, s) → TERM_SUB(m, s)
SUM_SUB(xi, Cons_sum(psi, k, s)) → SUM_SUB(xi, s)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(m, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(n, s)
SUM_SUB(xi, Cons_usual(y, m, s)) → SUM_SUB(xi, s)
TERM_SUB(Term_var(x), Cons_sum(xi, k, s)) → TERM_SUB(Term_var(x), s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(m, s)
CONCAT(Cons_sum(xi, k, s), t) → CONCAT(s, t)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(m, s)

The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB(Term_sub(m, s), t) → CONCAT(s, t)
TERM_SUB(Term_sub(m, s), t) → TERM_SUB(m, Concat(s, t))
TERM_SUB(Case(m, xi, n), s) → FROZEN(m, Sum_sub(xi, s), n, s)
TERM_SUB(Term_inl(m), s) → TERM_SUB(m, s)
TERM_SUB(Term_var(x), Cons_usual(y, m, s)) → TERM_SUB(Term_var(x), s)
CONCAT(Cons_usual(x, m, s), t) → CONCAT(s, t)
CONCAT(Concat(s, t), u) → CONCAT(s, Concat(t, u))
CONCAT(Cons_usual(x, m, s), t) → TERM_SUB(m, t)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(n, s)
TERM_SUB(Case(m, xi, n), s) → SUM_SUB(xi, s)
FROZEN(m, Sum_constant(Right), n, s) → TERM_SUB(n, s)
CONCAT(Concat(s, t), u) → CONCAT(t, u)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(n, s)
TERM_SUB(Term_inr(m), s) → TERM_SUB(m, s)
FROZEN(m, Sum_constant(Left), n, s) → TERM_SUB(m, s)
SUM_SUB(xi, Cons_sum(psi, k, s)) → SUM_SUB(xi, s)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(m, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(n, s)
SUM_SUB(xi, Cons_usual(y, m, s)) → SUM_SUB(xi, s)
TERM_SUB(Term_var(x), Cons_sum(xi, k, s)) → TERM_SUB(Term_var(x), s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(m, s)
CONCAT(Cons_sum(xi, k, s), t) → CONCAT(s, t)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(m, s)

The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB(Term_sub(m, s), t) → CONCAT(s, t)
TERM_SUB(Term_var(x), Cons_usual(y, m, s)) → TERM_SUB(Term_var(x), s)
TERM_SUB(Term_inl(m), s) → TERM_SUB(m, s)
TERM_SUB(Case(m, xi, n), s) → FROZEN(m, Sum_sub(xi, s), n, s)
TERM_SUB(Term_sub(m, s), t) → TERM_SUB(m, Concat(s, t))
CONCAT(Concat(s, t), u) → CONCAT(s, Concat(t, u))
CONCAT(Cons_usual(x, m, s), t) → CONCAT(s, t)
CONCAT(Cons_usual(x, m, s), t) → TERM_SUB(m, t)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(n, s)
TERM_SUB(Case(m, xi, n), s) → SUM_SUB(xi, s)
FROZEN(m, Sum_constant(Right), n, s) → TERM_SUB(n, s)
CONCAT(Concat(s, t), u) → CONCAT(t, u)
TERM_SUB(Term_inr(m), s) → TERM_SUB(m, s)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(n, s)
FROZEN(m, Sum_constant(Left), n, s) → TERM_SUB(m, s)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(m, s)
SUM_SUB(xi, Cons_sum(psi, k, s)) → SUM_SUB(xi, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(n, s)
TERM_SUB(Term_var(x), Cons_sum(xi, k, s)) → TERM_SUB(Term_var(x), s)
SUM_SUB(xi, Cons_usual(y, m, s)) → SUM_SUB(xi, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(m, s)
CONCAT(Cons_sum(xi, k, s), t) → CONCAT(s, t)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(m, s)

The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 3 SCCs with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SUM_SUB(xi, Cons_sum(psi, k, s)) → SUM_SUB(xi, s)
SUM_SUB(xi, Cons_usual(y, m, s)) → SUM_SUB(xi, s)

The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

SUM_SUB(xi, Cons_sum(psi, k, s)) → SUM_SUB(xi, s)

The remaining pairs can at least be oriented weakly.

SUM_SUB(xi, Cons_usual(y, m, s)) → SUM_SUB(xi, s)

Used ordering: Combined order from the following AFS and order.
SUM_SUB(x1, x2) = SUM_SUB(x2)
Cons_sum(x1, x2, x3) = Cons_sum(x3)
Cons_usual(x1, x2, x3) = x3

Lexicographic Path Order [19].
Precedence:

[SUM_SUB₁, Cons_{sum_1]}

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SUM_SUB(xi, Cons_usual(y, m, s)) → SUM_SUB(xi, s)

The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

SUM_SUB(xi, Cons_usual(y, m, s)) → SUM_SUB(xi, s)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
SUM_SUB(x1, x2) = SUM_SUB(x2)
Cons_usual(x1, x2, x3) = Cons_usual(x3)

Lexicographic Path Order [19].
Precedence:

Cons_usual₁ > SUM_SUB₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

              ↳ QDP

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB(Term_var(x), Cons_usual(y, m, s)) → TERM_SUB(Term_var(x), s)
TERM_SUB(Term_var(x), Cons_sum(xi, k, s)) → TERM_SUB(Term_var(x), s)

The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

TERM_SUB(Term_var(x), Cons_usual(y, m, s)) → TERM_SUB(Term_var(x), s)

The remaining pairs can at least be oriented weakly.

TERM_SUB(Term_var(x), Cons_sum(xi, k, s)) → TERM_SUB(Term_var(x), s)

Used ordering: Combined order from the following AFS and order.
TERM_SUB(x1, x2) = TERM_SUB(x2)
Term_var(x1) = x1
Cons_usual(x1, x2, x3) = Cons_usual(x3)
Cons_sum(x1, x2, x3) = x3

Lexicographic Path Order [19].
Precedence:

[TERM_SUB₁, Cons_{usual_1]}

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB(Term_var(x), Cons_sum(xi, k, s)) → TERM_SUB(Term_var(x), s)

The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

TERM_SUB(Term_var(x), Cons_sum(xi, k, s)) → TERM_SUB(Term_var(x), s)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
TERM_SUB(x1, x2) = TERM_SUB(x1, x2)
Term_var(x1) = Term_var(x1)
Cons_sum(x1, x2, x3) = Cons_sum(x2, x3)

Lexicographic Path Order [19].
Precedence:

TERM_SUB₂ > [Term_var₁, Cons_{sum_2]}

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB(Term_sub(m, s), t) → CONCAT(s, t)
TERM_SUB(Case(m, xi, n), s) → FROZEN(m, Sum_sub(xi, s), n, s)
TERM_SUB(Term_inl(m), s) → TERM_SUB(m, s)
TERM_SUB(Term_sub(m, s), t) → TERM_SUB(m, Concat(s, t))
CONCAT(Cons_usual(x, m, s), t) → CONCAT(s, t)
CONCAT(Concat(s, t), u) → CONCAT(s, Concat(t, u))
CONCAT(Cons_usual(x, m, s), t) → TERM_SUB(m, t)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(n, s)
FROZEN(m, Sum_constant(Right), n, s) → TERM_SUB(n, s)
CONCAT(Concat(s, t), u) → CONCAT(t, u)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(n, s)
TERM_SUB(Term_inr(m), s) → TERM_SUB(m, s)
FROZEN(m, Sum_constant(Left), n, s) → TERM_SUB(m, s)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(m, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(n, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(m, s)
CONCAT(Cons_sum(xi, k, s), t) → CONCAT(s, t)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(m, s)

The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

TERM_SUB(Term_sub(m, s), t) → CONCAT(s, t)
TERM_SUB(Case(m, xi, n), s) → FROZEN(m, Sum_sub(xi, s), n, s)
TERM_SUB(Term_inl(m), s) → TERM_SUB(m, s)
TERM_SUB(Term_sub(m, s), t) → TERM_SUB(m, Concat(s, t))
CONCAT(Cons_usual(x, m, s), t) → CONCAT(s, t)
CONCAT(Concat(s, t), u) → CONCAT(s, Concat(t, u))
CONCAT(Cons_usual(x, m, s), t) → TERM_SUB(m, t)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(n, s)
FROZEN(m, Sum_constant(Right), n, s) → TERM_SUB(n, s)
CONCAT(Concat(s, t), u) → CONCAT(t, u)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(n, s)
TERM_SUB(Term_inr(m), s) → TERM_SUB(m, s)
FROZEN(m, Sum_constant(Left), n, s) → TERM_SUB(m, s)
TERM_SUB(Term_app(m, n), s) → TERM_SUB(m, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(n, s)
FROZEN(m, Sum_term_var(xi), n, s) → TERM_SUB(m, s)
CONCAT(Cons_sum(xi, k, s), t) → CONCAT(s, t)
TERM_SUB(Term_pair(m, n), s) → TERM_SUB(m, s)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
TERM_SUB(x1, x2) = x1
Term_sub(x1, x2) = Term_sub(x1, x2)
CONCAT(x1, x2) = CONCAT(x1)
Case(x1, x2, x3) = Case(x1, x2, x3)
FROZEN(x1, x2, x3, x4) = FROZEN(x1, x2, x3)
Sum_sub(x1, x2) = x1
Term_inl(x1) = Term_inl(x1)
Concat(x1, x2) = Concat(x1, x2)
Cons_usual(x1, x2, x3) = Cons_usual(x2, x3)
Term_app(x1, x2) = Term_app(x1, x2)
Sum_constant(x1) = Sum_constant
Right = Right
Term_pair(x1, x2) = Term_pair(x1, x2)
Term_inr(x1) = Term_inr(x1)
Left = Left
Sum_term_var(x1) = Sum_term_var
Cons_sum(x1, x2, x3) = Cons_sum(x1, x2, x3)
Frozen(x1, x2, x3, x4) = x2
Id = Id
Term_var(x1) = x1

Lexicographic Path Order [19].
Precedence:

Case₃ > [FROZEN₃, Sum_constant, Sum_{term_var]}
Term_inl₁ > [Term_sub₂, Term_{inr_1]} > CONCAT₁ > Concat₂ > Cons_usual₂ > [FROZEN₃, Sum_constant, Sum_{term_var]}
Term_inl₁ > [Term_sub₂, Term_{inr_1]} > CONCAT₁ > Concat₂ > Cons_sum₃ > [FROZEN₃, Sum_constant, Sum_{term_var]}
Term_inl₁ > [Term_sub₂, Term_{inr_1]} > Term_app₂ > [FROZEN₃, Sum_constant, Sum_{term_var]}
Right > [FROZEN₃, Sum_constant, Sum_{term_var]}
Term_pair₂ > [Term_sub₂, Term_{inr_1]} > CONCAT₁ > Concat₂ > Cons_usual₂ > [FROZEN₃, Sum_constant, Sum_{term_var]}
Term_pair₂ > [Term_sub₂, Term_{inr_1]} > CONCAT₁ > Concat₂ > Cons_sum₃ > [FROZEN₃, Sum_constant, Sum_{term_var]}
Term_pair₂ > [Term_sub₂, Term_{inr_1]} > Term_app₂ > [FROZEN₃, Sum_constant, Sum_{term_var]}
Left > [FROZEN₃, Sum_constant, Sum_{term_var]}
Id > [FROZEN₃, Sum_constant, Sum_{term_var]}

The following usable rules [14] were oriented:

Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ EdgeDeletionProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

Term_sub(Case(m, xi, n), s) → Frozen(m, Sum_sub(xi, s), n, s)
Frozen(m, Sum_constant(Left), n, s) → Term_sub(m, s)
Frozen(m, Sum_constant(Right), n, s) → Term_sub(n, s)
Frozen(m, Sum_term_var(xi), n, s) → Case(Term_sub(m, s), xi, Term_sub(n, s))
Term_sub(Term_app(m, n), s) → Term_app(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_pair(m, n), s) → Term_pair(Term_sub(m, s), Term_sub(n, s))
Term_sub(Term_inl(m), s) → Term_inl(Term_sub(m, s))
Term_sub(Term_inr(m), s) → Term_inr(Term_sub(m, s))
Term_sub(Term_var(x), Id) → Term_var(x)
Term_sub(Term_var(x), Cons_usual(y, m, s)) → m
Term_sub(Term_var(x), Cons_usual(y, m, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_var(x), Cons_sum(xi, k, s)) → Term_sub(Term_var(x), s)
Term_sub(Term_sub(m, s), t) → Term_sub(m, Concat(s, t))
Sum_sub(xi, Id) → Sum_term_var(xi)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_constant(k)
Sum_sub(xi, Cons_sum(psi, k, s)) → Sum_sub(xi, s)
Sum_sub(xi, Cons_usual(y, m, s)) → Sum_sub(xi, s)
Concat(Concat(s, t), u) → Concat(s, Concat(t, u))
Concat(Cons_usual(x, m, s), t) → Cons_usual(x, Term_sub(m, t), Concat(s, t))
Concat(Cons_sum(xi, k, s), t) → Cons_sum(xi, k, Concat(s, t))
Concat(Id, s) → s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.